$\vdash$  $\forall$$A$:Type, $x$,$y$:$A$. $x$ $\neq$ $y$ $\in$ $A$  $\in$ $\mathbb{P}$